Bob is cold. Bob is smart. Charlie is cold. Erin is cold. Erin is quiet. Erin is red. Erin is not smart. Gary is blue. Gary is red. Gary is rough. If Bob is not cold then Bob is quiet. Smart things are blue. If something is rough and blue then it is not smart. If something is blue and not rough then it is not furry. If something is blue and not smart then it is furry. If something is furry then it is red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Bob is not cold then Bob is quiet.
((("Bob" "is" "cold" "~")) -> ("Bob" "is" "quiet" "+"))
Smart things are blue.
((("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
If something is rough and blue then it is not smart.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "smart" "-"))
If something is blue and not rough then it is not furry.
((("something" "is" "blue" "+") ("something" "is" "rough" "~")) -> ("something" "is" "furry" "-"))
If something is blue and not smart then it is furry.
((("something" "is" "blue" "+") ("something" "is" "smart" "~")) -> ("something" "is" "furry" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Gary is blue.
True
1
proof
[(triple8)]
("Gary" "is" "blue" "+")
triple8
Gary is not rough.
False
1
inv-proof
[(triple10)]
("Gary" "is" "rough" "-")
triple10
Gary is not smart.
True
3
proof
[(((triple10 triple8) -> rule3))]
("Gary" "is" "smart" "-")
((triple10 triple8) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is smart.
False
3
inv-proof
[(((triple10 triple8) -> rule3))]
("Gary" "is" "smart" "+")
((triple10 triple8) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is furry.
True
5
proof
[(((triple8 ((triple10 triple8) -> rule3)) -> rule5))]
("Gary" "is" "furry" "+")
((triple8 ((triple10 triple8) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not smart.
("Gary" "is" "smart" "-")
int2
Gary is not furry.
False
5
inv-proof
[(((triple8 ((triple10 triple8) -> rule3)) -> rule5))]
("Gary" "is" "furry" "-")
((triple8 ((triple10 triple8) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not smart.
("Gary" "is" "smart" "-")
int2
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Erin is furry.
Unknown
rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "furry" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Bob is cold.[(triple1)] Bob is smart.[(triple2)] Charlie is cold.[(triple3)] Erin is cold.[(triple4)] Erin is not smart.[(triple7)] Erin is quiet.[(triple5)] Erin is red.[(triple6)] Gary is blue.[(triple8)] Gary is red.[(triple9 OR ((((triple8 ((triple10 triple8) -> rule3)) -> rule5)) -> rule6))] Gary is rough.[(triple10)] @1: Bob is blue.[(((triple2) -> rule2))] Gary is not smart.[(((triple10 triple8) -> rule3))] @2: Gary is furry.[(((triple8 ((triple10 triple8) -> rule3)) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is not smart.
("Erin" "is" "smart" "-")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
((((triple8 ((triple10 triple8) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not smart.
("Gary" "is" "smart" "-")
int3
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is not smart.
("Gary" "is" "smart" "-")
((triple10 triple8) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple8 ((triple10 triple8) -> (rule3 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not smart.
("Gary" "is" "smart" "-")
int2