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