Anne is cold. Anne is red. Anne is rough. Anne is not young. Bob is not big. Bob is blue. Bob is not young. Fiona is green. Fiona is red. Gary is green. Gary is not red. Gary is rough. Red, blue people are green. Blue people are green. If Bob is cold and Bob is not young then Bob is rough. Young people are not blue. If someone is blue and big then they are cold. All green people are cold. If Anne is not young then Anne is not green. If Gary is green then Gary is not red.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not young.
("Anne" "is" "young" "-")
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not young.
("Bob" "is" "young" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is not red.
("Gary" "is" "red" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Red, blue people are green.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If Bob is cold and Bob is not young then Bob is rough.
((("Bob" "is" "cold" "+") ("Bob" "is" "young" "~")) -> ("Bob" "is" "rough" "+"))
Young people are not blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "-"))
If someone is blue and big then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Anne is not young then Anne is not green.
((("Anne" "is" "young" "~")) -> ("Anne" "is" "green" "-"))
If Gary is green then Gary is not red.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "red" "-"))
Gary is not red.
True
1
proof
[(triple11 OR ((triple10) -> rule8))]
("Gary" "is" "red" "-")
triple11
((triple10) -> (rule8 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Bob is young.
False
1
inv-proof
[(triple7)]
("Bob" "is" "young" "+")
triple7
Gary is cold.
True
2
proof
[(((triple10) -> rule6))]
("Gary" "is" "cold" "+")
((triple10) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Fiona is not cold.
False
2
inv-proof
[(((triple8) -> rule6))]
("Fiona" "is" "cold" "-")
((triple8) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Bob is cold.
True
3
proof
[(((((triple6) -> rule2)) -> rule6))]
("Bob" "is" "cold" "+")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule6))]
("Bob" "is" "cold" "-")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
True
5
proof
[(((((((triple6) -> rule2)) -> rule6) triple7) -> rule3))]
("Bob" "is" "rough" "+")
((((((triple6) -> (rule2 % int3))) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not rough.
False
5
inv-proof
[(((((((triple6) -> rule2)) -> rule6) triple7) -> rule3))]
("Bob" "is" "rough" "-")
((((((triple6) -> (rule2 % int3))) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Fiona is blue.
Unknown
random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Anne is cold.[(triple1)] Anne is not young.[(triple4)] Anne is red.[(triple2)] Anne is rough.[(triple3)] Bob is blue.[(triple6)] Bob is not big.[(triple5)] Bob is not young.[(triple7)] Fiona is green.[(triple8)] Fiona is red.[(triple9)] Gary is green.[(triple10)] Gary is not red.[(triple11 OR ((triple10) -> rule8))] Gary is rough.[(triple12)] @1: Anne is not green.[(((triple4) -> rule7))] Bob is green.[(((triple6) -> rule2))] Fiona is cold.[(((triple8) -> rule6))] Gary is cold.[(((triple10) -> rule6))] @2: Bob is cold.[(((((triple6) -> rule2)) -> rule6))] @3: Bob is rough.[(((((((triple6) -> rule2)) -> rule6) triple7) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is not young.
("Anne" "is" "young" "-")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple6
Bob is not big.
("Bob" "is" "big" "-")
triple5
Bob is not young.
("Bob" "is" "young" "-")
triple7
Fiona is green.
("Fiona" "is" "green" "+")
triple8
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is not red.
("Gary" "is" "red" "-")
triple11
((triple10) -> (rule8 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Anne is not green.
("Anne" "is" "green" "-")
((triple4) -> (rule7 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple6) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple8) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple10) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple6) -> (rule2 % int3))) -> (rule6 % int2)) triple7) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3