Erin is red. Erin is round. Erin is smart. Erin is white. Erin is not young. Gary is not big. Gary is not smart. Gary is not young. Harry is big. Harry is red. Harry is smart. Harry is white. If Erin is not white then Erin is smart. If someone is big then they are smart. All young, rough people are not round. If someone is rough and not smart then they are round. All white people are round. If Harry is round then Harry is rough.
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is not young.
("Erin" "is" "young" "-")
Gary is not big.
("Gary" "is" "big" "-")
Gary is not smart.
("Gary" "is" "smart" "-")
Gary is not young.
("Gary" "is" "young" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If Erin is not white then Erin is smart.
((("Erin" "is" "white" "~")) -> ("Erin" "is" "smart" "+"))
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All young, rough people are not round.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "-"))
If someone is rough and not smart then they are round.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "round" "+"))
All white people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If Harry is round then Harry is rough.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "rough" "+"))
Erin is round.
True
1
proof
[(triple2 OR ((triple4) -> rule5))]
("Erin" "is" "round" "+")
triple2
((triple4) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is not red.
False
1
inv-proof
[(triple10)]
("Harry" "is" "red" "-")
triple10
Harry is round.
True
2
proof
[(((triple12) -> rule5))]
("Harry" "is" "round" "+")
((triple12) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple12) -> rule5))]
("Harry" "is" "round" "-")
((triple12) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
True
3
proof
[(((((triple12) -> rule5)) -> rule6))]
("Harry" "is" "rough" "+")
((((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple12) -> rule5)) -> rule6))]
("Harry" "is" "rough" "-")
((((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "round" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Erin is not young.[(triple5)] Erin is red.[(triple1)] Erin is round.[(triple2 OR ((triple4) -> rule5))] Erin is smart.[(triple3)] Erin is white.[(triple4)] Gary is not big.[(triple6)] Gary is not smart.[(triple7)] Gary is not young.[(triple8)] Harry is big.[(triple9)] Harry is red.[(triple10)] Harry is smart.[(triple11 OR ((triple9) -> rule2))] Harry is white.[(triple12)] @1: Harry is round.[(((triple12) -> rule5))] @2: Harry is rough.[(((((triple12) -> rule5)) -> rule6))]
Erin is not young.
("Erin" "is" "young" "-")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
((triple4) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Erin is white.
("Erin" "is" "white" "+")
triple4
Gary is not big.
("Gary" "is" "big" "-")
triple6
Gary is not smart.
("Gary" "is" "smart" "-")
triple7
Gary is not young.
("Gary" "is" "young" "-")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is red.
("Harry" "is" "red" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
((triple12) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple12) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2