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