Bob is furry. Bob is round. Bob is young. Charlie is blue. Charlie is green. Charlie is white. Charlie is young. Harry is cold. Harry is green. Harry is white. If something is green and round then it is young. If something is white then it is cold. If something is cold then it is round.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is green and round then it is young.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is cold then it is round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Charlie is white.
True
1
proof
[(triple6)]
("Charlie" "is" "white" "+")
triple6
Harry is not white.
False
1
inv-proof
[(triple10)]
("Harry" "is" "white" "-")
triple10
Harry is round.
True
2
proof
[(((triple8) -> rule3) OR ((((triple10) -> rule2)) -> rule3))]
("Harry" "is" "round" "+")
((triple8) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Charlie is not cold.
False
2
inv-proof
[(((triple6) -> rule2))]
("Charlie" "is" "cold" "-")
((triple6) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Harry is young.
True
4
proof
[(((triple9 ((triple8) -> rule3)) -> rule1) OR ((triple9 ((((triple10) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "young" "+")
((triple9 ((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple9 ((((triple10) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not young.
False
4
inv-proof
[(((triple9 ((triple8) -> rule3)) -> rule1) OR ((triple9 ((((triple10) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "young" "-")
((triple9 ((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple9 ((((triple10) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is furry.[(triple1)] Bob is round.[(triple2)] Bob is young.[(triple3)] Charlie is blue.[(triple4)] Charlie is green.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7 OR ((triple5 ((((triple6) -> rule2)) -> rule3)) -> rule1))] Harry is cold.[(triple8 OR ((triple10) -> rule2))] Harry is green.[(triple9)] Harry is white.[(triple10)] @1: Charlie is cold.[(((triple6) -> rule2))] Harry is round.[(((triple8) -> rule3) OR ((((triple10) -> rule2)) -> rule3))] @2: Charlie is round.[(((((triple6) -> rule2)) -> rule3))] Harry is young.[(((triple9 ((triple8) -> rule3)) -> rule1) OR ((triple9 ((((triple10) -> rule2)) -> rule3)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple5 ((((triple6) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
triple8
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple6) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple8) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple9 ((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((triple9 ((((triple10) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3