Anne is cold. Anne is rough. Bob is blue. Bob is green. Bob is nice. Bob is quiet. Fiona is big. Fiona is blue. Fiona is rough. Gary is big. Gary is blue. Gary is cold. Gary is green. Gary is quiet. Gary is rough. All rough things are big. Blue, green things are big. If something is quiet and rough then it is big. If something is green and cold then it is nice. If Gary is big then Gary is cold. If something is nice and green then it is quiet.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Blue, green things are big.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is quiet and rough then it is big.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is green and cold then it is nice.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If Gary is big then Gary is cold.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "cold" "+"))
If something is nice and green then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Gary is big.
True
1
proof
[(triple10 OR ((triple15) -> rule1) OR ((triple11 triple13) -> rule2) OR ((triple14 triple15) -> rule3) OR ((((((triple13 triple12) -> rule4) triple13) -> rule6) triple15) -> rule3))]
("Gary" "is" "big" "+")
triple10
((triple15) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple11 triple13) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple14 triple15) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((((triple13 triple12) -> (rule4 % int3)) triple13) -> (rule6 % int2)) triple15) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Bob is not nice.
False
1
inv-proof
[(triple5)]
("Bob" "is" "nice" "-")
triple5
Anne is big.
True
2
proof
[(((triple2) -> rule1))]
("Anne" "is" "big" "+")
((triple2) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Gary is not nice.
False
3
inv-proof
[(((triple13 triple12) -> rule4) OR ((triple13 ((triple10) -> rule5)) -> rule4) OR ((triple13 ((((triple15) -> rule1)) -> rule5)) -> rule4) OR ((triple13 ((((triple11 triple13) -> rule2)) -> rule5)) -> rule4) OR ((triple13 ((((triple14 triple15) -> rule3)) -> rule5)) -> rule4))]
("Gary" "is" "nice" "-")
((triple13 triple12) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple13 ((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((triple13 ((((triple15) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple13 ((((triple11 triple13) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple13 ((((triple14 triple15) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "nice" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "quiet" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Anne is rough.[(triple2)] Bob is blue.[(triple3)] Bob is green.[(triple4)] Bob is nice.[(triple5)] Bob is quiet.[(triple6 OR ((triple5 triple4) -> rule6))] Fiona is big.[(triple7 OR ((triple9) -> rule1))] Fiona is blue.[(triple8)] Fiona is rough.[(triple9)] Gary is big.[(triple10 OR ((triple15) -> rule1) OR ((triple11 triple13) -> rule2) OR ((triple14 triple15) -> rule3) OR ((((((triple13 triple12) -> rule4) triple13) -> rule6) triple15) -> rule3))] Gary is blue.[(triple11)] Gary is cold.[(triple12 OR ((triple10) -> rule5) OR ((((triple15) -> rule1)) -> rule5) OR ((((triple11 triple13) -> rule2)) -> rule5) OR ((((triple14 triple15) -> rule3)) -> rule5))] Gary is green.[(triple13)] Gary is quiet.[(triple14 OR ((((triple13 triple12) -> rule4) triple13) -> rule6) OR ((((triple13 ((triple10) -> rule5)) -> rule4) triple13) -> rule6) OR ((((triple13 ((((triple15) -> rule1)) -> rule5)) -> rule4) triple13) -> rule6) OR ((((triple13 ((((triple11 triple13) -> rule2)) -> rule5)) -> rule4) triple13) -> rule6))] Gary is rough.[(triple15)] @1: Anne is big.[(((triple2) -> rule1))] Bob is big.[(((triple3 triple4) -> rule2))] Gary is nice.[(((triple13 triple12) -> rule4) OR ((triple13 ((triple10) -> rule5)) -> rule4) OR ((triple13 ((((triple15) -> rule1)) -> rule5)) -> rule4) OR ((triple13 ((((triple11 triple13) -> rule2)) -> rule5)) -> rule4) OR ((triple13 ((((triple14 triple15) -> rule3)) -> rule5)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
triple5
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
((triple5 triple4) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple7
((triple9) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
Fiona is rough.
("Fiona" "is" "rough" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
((triple15) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple11 triple13) -> (rule2 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple14 triple15) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((((triple13 triple12) -> (rule4 % int3)) triple13) -> (rule6 % int2)) triple15) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
triple11
Gary is cold.
("Gary" "is" "cold" "+")
triple12
((triple10) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple15) -> (rule1 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple11 triple13) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
((((triple14 triple15) -> (rule3 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple13
Gary is quiet.
("Gary" "is" "quiet" "+")
triple14
((((triple13 triple12) -> (rule4 % int2)) triple13) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple13 ((triple10) -> (rule5 % int3))) -> (rule4 % int2)) triple13) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
((((triple13 ((((triple15) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple13) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
((((triple13 ((((triple11 triple13) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) triple13) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
triple15
Anne is big.
("Anne" "is" "big" "+")
((triple2) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple3 triple4) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple13 triple12) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple13 ((triple10) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
((triple13 ((((triple15) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple13 ((((triple11 triple13) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
((triple13 ((((triple14 triple15) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3