Bob is quiet. Charlie is furry. Erin is blue. Erin is furry. Erin is nice. Erin is white. Gary is cold. If something is cold then it is big. Cold, big things are white. If something is big and white then it is furry.
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If something is cold then it is big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Cold, big things are white.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is big and white then it is furry.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Charlie is furry.
True
1
proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Gary is big.
True
2
proof
[(((triple7) -> rule1))]
("Gary" "is" "big" "+")
((triple7) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not big.
False
2
inv-proof
[(((triple7) -> rule1))]
("Gary" "is" "big" "-")
((triple7) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
True
4
proof
[(((triple7 ((triple7) -> rule1)) -> rule2))]
("Gary" "is" "white" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not white.
False
4
inv-proof
[(((triple7 ((triple7) -> rule1)) -> rule2))]
("Gary" "is" "white" "-")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "white" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "big" "+")
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Bob is quiet.[(triple1)] Charlie is furry.[(triple2)] Erin is blue.[(triple3)] Erin is furry.[(triple4)] Erin is nice.[(triple5)] Erin is white.[(triple6)] Gary is cold.[(triple7)] @1: Gary is big.[(((triple7) -> rule1))] @2: Gary is white.[(((triple7 ((triple7) -> rule1)) -> rule2))] @3: Gary is furry.[(((((triple7) -> rule1) ((triple7 ((triple7) -> rule1)) -> rule2)) -> rule3))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Gary is cold.
("Gary" "is" "cold" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
((triple7) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple7 ((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple7) -> (rule1 % int3)) ((triple7 ((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3