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