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