Anne is kind. Anne is rough. Bob is green. Bob is white. Bob is not young. Charlie is big. Charlie is cold. Charlie is green. Charlie is not kind. Charlie is rough. Charlie is young. Dave is not big. Dave is cold. Dave is kind. Dave is white. Dave is young. If Anne is big and Anne is rough then Anne is cold. If Anne is kind then Anne is cold. Cold, kind people are green. Big, white people are green. If someone is kind and not rough then they are not big. All green people are white. Green, kind people are white. If someone is green and not rough then they are young.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is not young.
("Bob" "is" "young" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If Anne is big and Anne is rough then Anne is cold.
((("Anne" "is" "big" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "cold" "+"))
If Anne is kind then Anne is cold.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "cold" "+"))
Cold, kind people are green.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Big, white people are green.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is kind and not rough then they are not big.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "big" "-"))
All green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Green, kind people are white.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If someone is green and not rough then they are young.
((("someone" "is" "green" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "young" "+"))
Dave is not big.
True
1
proof
[(triple12)]
("Dave" "is" "big" "-")
triple12
Dave is not white.
False
1
inv-proof
[(triple15 OR ((((triple13 triple14) -> rule3)) -> rule6) OR ((((triple13 triple14) -> rule3) triple14) -> rule7))]
("Dave" "is" "white" "-")
triple15
((((triple13 triple14) -> (rule3 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple13 triple14) -> (rule3 % int2)) triple14) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is green.
True
3
proof
[(((triple13 triple14) -> rule3))]
("Dave" "is" "green" "+")
((triple13 triple14) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple8) -> rule6))]
("Charlie" "is" "white" "-")
((triple8) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Anne is green.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule3))]
("Anne" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not green.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule3))]
("Anne" "is" "green" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
True
5
proof
[(((((((triple1) -> rule2) triple1) -> rule3)) -> rule6) OR ((((((triple1) -> rule2) triple1) -> rule3) triple1) -> rule7))]
("Anne" "is" "white" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not white.
False
5
inv-proof
[(((((((triple1) -> rule2) triple1) -> rule3)) -> rule6) OR ((((((triple1) -> rule2) triple1) -> rule3) triple1) -> rule7))]
("Anne" "is" "white" "-")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "young" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is kind.[(triple1)] Anne is rough.[(triple2)] Bob is green.[(triple3)] Bob is not young.[(triple5)] Bob is white.[(triple4 OR ((triple3) -> rule6))] Charlie is big.[(triple6)] Charlie is cold.[(triple7)] Charlie is green.[(triple8)] Charlie is not kind.[(triple9)] Charlie is rough.[(triple10)] Charlie is young.[(triple11)] Dave is cold.[(triple13)] Dave is kind.[(triple14)] Dave is not big.[(triple12)] Dave is white.[(triple15 OR ((((triple13 triple14) -> rule3)) -> rule6) OR ((((triple13 triple14) -> rule3) triple14) -> rule7))] Dave is young.[(triple16)] @1: Anne is cold.[(((triple1) -> rule2))] Charlie is white.[(((triple8) -> rule6))] Dave is green.[(((triple13 triple14) -> rule3))] @2: Anne is green.[(((((triple1) -> rule2) triple1) -> rule3))] @3: Anne is white.[(((((((triple1) -> rule2) triple1) -> rule3)) -> rule6) OR ((((((triple1) -> rule2) triple1) -> rule3) triple1) -> rule7))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Bob is not young.
("Bob" "is" "young" "-")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple3) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
triple8
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple9
Charlie is rough.
("Charlie" "is" "rough" "+")
triple10
Charlie is young.
("Charlie" "is" "young" "+")
triple11
Dave is cold.
("Dave" "is" "cold" "+")
triple13
Dave is kind.
("Dave" "is" "kind" "+")
triple14
Dave is not big.
("Dave" "is" "big" "-")
triple12
Dave is white.
("Dave" "is" "white" "+")
triple15
((((triple13 triple14) -> (rule3 % int2))) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple13 triple14) -> (rule3 % int2)) triple14) -> (rule7 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple16
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple8) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple13 triple14) -> (rule3 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2)) triple1) -> (rule7 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3