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