Dave is big. Dave is cold. Erin is red. Erin is rough. Gary is big. Gary is quiet. Gary is rough. Kind people are round. All big people are round. If someone is round and big then they are rough. All cold, rough people are round. All red, round people are kind. All quiet people are big.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Kind people are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
All big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is round and big then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
All cold, rough people are round.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
All red, round people are kind.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
All quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Gary is big.
True
1
proof
[(triple5 OR ((triple6) -> rule6))]
("Gary" "is" "big" "+")
triple5
((triple6) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Erin is not rough.
False
1
inv-proof
[(triple4)]
("Erin" "is" "rough" "-")
triple4
Gary is round.
True
2
proof
[(((triple5) -> rule2) OR ((((triple6) -> rule6)) -> rule2))]
("Gary" "is" "round" "+")
((triple5) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not round.
False
2
inv-proof
[(((triple5) -> rule2) OR ((((triple6) -> rule6)) -> rule2))]
("Gary" "is" "round" "-")
((triple5) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "kind" "-")
Erin is round.
Unknown
rconc
[@4: Erin is round.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule2 <- rule6 <- FAIL)]]
("Erin" "is" "round" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is big.[(triple1)] Dave is cold.[(triple2)] Erin is red.[(triple3)] Erin is rough.[(triple4)] Gary is big.[(triple5 OR ((triple6) -> rule6))] Gary is quiet.[(triple6)] Gary is rough.[(triple7 OR ((((triple5) -> rule2) triple5) -> rule3) OR ((((triple5) -> rule2) ((triple6) -> rule6)) -> rule3) OR ((((((triple6) -> rule6)) -> rule2) triple5) -> rule3) OR ((((((triple6) -> rule6)) -> rule2) ((triple6) -> rule6)) -> rule3))] @1: Dave is round.[(((triple1) -> rule2))] Gary is round.[(((triple5) -> rule2) OR ((((triple6) -> rule6)) -> rule2))] @2: Dave is rough.[(((((triple1) -> rule2) triple1) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
((triple6) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
((((triple5) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple5) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2)) ((triple6) -> (rule6 % int3))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple5) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2