Charlie is nice. Charlie is smart. Dave is round. Erin is not big. Erin is nice. Erin is not smart. Gary is cold. Gary is nice. Gary is rough. Gary is smart. If someone is round and big then they are not rough. If Gary is not big then Gary is cold. If Charlie is blue then Charlie is big. If Charlie is blue then Charlie is not cold. If Erin is nice then Erin is round. If someone is round then they are blue.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is round and big then they are not rough.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "-"))
If Gary is not big then Gary is cold.
((("Gary" "is" "big" "~")) -> ("Gary" "is" "cold" "+"))
If Charlie is blue then Charlie is big.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "big" "+"))
If Charlie is blue then Charlie is not cold.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "cold" "-"))
If Erin is nice then Erin is round.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "round" "+"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Gary is rough.
True
1
proof
[(triple9)]
("Gary" "is" "rough" "+")
triple9
Charlie is not nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "-")
triple1
Dave is blue.
True
2
proof
[(((triple3) -> rule6))]
("Dave" "is" "blue" "+")
((triple3) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple5) -> rule5))]
("Erin" "is" "round" "-")
((triple5) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is blue.
True
3
proof
[(((((triple5) -> rule5)) -> rule6))]
("Erin" "is" "blue" "+")
((((triple5) -> (rule5 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule6))]
("Erin" "is" "blue" "-")
((((triple5) -> (rule5 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Charlie is not big.
Unknown
inv-rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "big" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is nice.[(triple1)] Charlie is smart.[(triple2)] Dave is round.[(triple3)] Erin is nice.[(triple5)] Erin is not big.[(triple4)] Erin is not smart.[(triple6)] Gary is cold.[(triple7)] Gary is nice.[(triple8)] Gary is rough.[(triple9)] Gary is smart.[(triple10)] @1: Dave is blue.[(((triple3) -> rule6))] Erin is round.[(((triple5) -> rule5))] @2: Erin is blue.[(((((triple5) -> rule5)) -> rule6))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is not big.
("Erin" "is" "big" "-")
triple4
Erin is not smart.
("Erin" "is" "smart" "-")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Dave is blue.
("Dave" "is" "blue" "+")
((triple3) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple5) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((((triple5) -> (rule5 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2