Anne is kind. Anne is nice. Anne is red. Anne is smart. Anne is young. Charlie is furry. Charlie is kind. Charlie is red. Charlie is smart. Dave is furry. Dave is kind. Dave is nice. Dave is red. Harry is red. Harry is smart. All red things are young. All furry things are blue. All nice things are furry. If Harry is blue and Harry is nice then Harry is red. Blue, young things are red. All kind things are red. If something is kind then it is nice. Blue things are nice.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All furry things are blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
All nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If Harry is blue and Harry is nice then Harry is red.
((("Harry" "is" "blue" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "red" "+"))
Blue, young things are red.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Anne is smart.
True
1
proof
[(triple4)]
("Anne" "is" "smart" "+")
triple4
Anne is not nice.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule7))]
("Anne" "is" "nice" "-")
triple2
((triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Charlie is young.
True
2
proof
[(((triple8) -> rule1) OR ((((triple7) -> rule6)) -> rule1))]
("Charlie" "is" "young" "+")
((triple8) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Dave is not blue.
False
2
inv-proof
[(((triple10) -> rule2) OR ((((triple12) -> rule3)) -> rule2) OR ((((((triple11) -> rule7)) -> rule3)) -> rule2))]
("Dave" "is" "blue" "-")
((triple10) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple11) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Harry is not blue.
Unknown
inv-rconc
[@3: Harry is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule7 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is nice.
Unknown
rconc
[@4: Harry is nice.[CWA. Example of deepest failure = (rule8 <- rule2 <- rule3 <- rule7 <- FAIL)]]
("Harry" "is" "nice" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is nice.[(triple2 OR ((triple1) -> rule7))] Anne is red.[(triple3 OR ((triple1) -> rule6) OR ((((((triple2) -> rule3)) -> rule2) triple5) -> rule5) OR ((((((((triple1) -> rule7)) -> rule3)) -> rule2) triple5) -> rule5))] Anne is smart.[(triple4)] Anne is young.[(triple5 OR ((triple3) -> rule1) OR ((((triple1) -> rule6)) -> rule1))] Charlie is furry.[(triple6 OR ((((triple7) -> rule7)) -> rule3))] Charlie is kind.[(triple7)] Charlie is red.[(triple8 OR ((triple7) -> rule6))] Charlie is smart.[(triple9)] Dave is furry.[(triple10 OR ((triple12) -> rule3) OR ((((triple11) -> rule7)) -> rule3))] Dave is kind.[(triple11)] Dave is nice.[(triple12 OR ((triple11) -> rule7) OR ((((triple10) -> rule2)) -> rule8))] Dave is red.[(triple13 OR ((triple11) -> rule6))] Harry is red.[(triple14)] Harry is smart.[(triple15)] @1: Anne is furry.[(((triple2) -> rule3) OR ((((triple1) -> rule7)) -> rule3))] Charlie is blue.[(((triple6) -> rule2) OR ((((((triple7) -> rule7)) -> rule3)) -> rule2))] Charlie is nice.[(((triple7) -> rule7) OR ((((triple6) -> rule2)) -> rule8))] Charlie is young.[(((triple8) -> rule1) OR ((((triple7) -> rule6)) -> rule1))] Dave is blue.[(((triple10) -> rule2) OR ((((triple12) -> rule3)) -> rule2) OR ((((((triple11) -> rule7)) -> rule3)) -> rule2))] Dave is young.[(((triple13) -> rule1) OR ((((triple11) -> rule6)) -> rule1))] Harry is young.[(((triple14) -> rule1))] @2: Anne is blue.[(((((triple2) -> rule3)) -> rule2) OR ((((((triple1) -> rule7)) -> rule3)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple1) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple1) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((((((triple1) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
((triple3) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
((((triple7) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple8
((triple7) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple9
Dave is furry.
("Dave" "is" "furry" "+")
triple10
((triple12) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple11) -> (rule7 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple11
Dave is nice.
("Dave" "is" "nice" "+")
triple12
((triple11) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple13
((triple11) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple6) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple7) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((triple8) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple10) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple11) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((triple13) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple11) -> (rule6 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((triple14) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((((((triple1) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3