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