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