Anne is blue. Anne is cold. Anne is furry. Bob is young. Charlie is cold. Charlie is green. Dave is cold. Dave is furry. Dave is green. Dave is kind. If Charlie is young and Charlie is green then Charlie is cold. All blue people are cold. All green, young people are smart. If Dave is smart then Dave is furry. Smart, kind people are cold. If someone is smart then they are blue. All furry, green people are young. If Dave is green and Dave is young then Dave is cold.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
If Charlie is young and Charlie is green then Charlie is cold.
((("Charlie" "is" "young" "+") ("Charlie" "is" "green" "+")) -> ("Charlie" "is" "cold" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All green, young people are smart.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If Dave is smart then Dave is furry.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "furry" "+"))
Smart, kind people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
All furry, green people are young.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If Dave is green and Dave is young then Dave is cold.
((("Dave" "is" "green" "+") ("Dave" "is" "young" "+")) -> ("Dave" "is" "cold" "+"))
Dave is furry.
True
1
proof
[(triple8)]
("Dave" "is" "furry" "+")
triple8
Anne is not cold.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule2))]
("Anne" "is" "cold" "-")
triple2
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Dave is young.
True
3
proof
[(((triple8 triple9) -> rule7))]
("Dave" "is" "young" "+")
((triple8 triple9) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
3
inv-proof
[(((triple8 triple9) -> rule7))]
("Dave" "is" "young" "-")
((triple8 triple9) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
True
5
proof
[(((triple9 ((triple8 triple9) -> rule7)) -> rule3))]
("Dave" "is" "smart" "+")
((triple9 ((triple8 triple9) -> (rule7 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not smart.
False
5
inv-proof
[(((triple9 ((triple8 triple9) -> rule7)) -> rule3))]
("Dave" "is" "smart" "-")
((triple9 ((triple8 triple9) -> (rule7 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Bob" "is" "blue" "-")
Charlie is smart.
Unknown
rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Charlie" "is" "smart" "+")
Bob is not cold.
Unknown
inv-rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule3 <- FAIL)]]
("Bob" "is" "cold" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2 OR ((triple1) -> rule2))] Anne is furry.[(triple3)] Bob is young.[(triple4)] Charlie is cold.[(triple5)] Charlie is green.[(triple6)] Dave is cold.[(triple7 OR ((triple9 ((triple8 triple9) -> rule7)) -> rule8) OR ((((triple9 ((triple8 triple9) -> rule7)) -> rule3) triple10) -> rule5) OR ((((((triple9 ((triple8 triple9) -> rule7)) -> rule3)) -> rule6)) -> rule2))] Dave is furry.[(triple8)] Dave is green.[(triple9)] Dave is kind.[(triple10)] @1: Dave is young.[(((triple8 triple9) -> rule7))] @2: Dave is smart.[(((triple9 ((triple8 triple9) -> rule7)) -> rule3))] @3: Dave is blue.[(((((triple9 ((triple8 triple9) -> rule7)) -> rule3)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
((triple9 ((triple8 triple9) -> (rule7 % int2))) -> (rule8 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple9 ((triple8 triple9) -> (rule7 % int3))) -> (rule3 % int2)) triple10) -> (rule5 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple9 ((triple8 triple9) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
((triple8 triple9) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple9 ((triple8 triple9) -> (rule7 % int2))) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple9 ((triple8 triple9) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3