Anne is big. Anne is cold. Anne is red. Bob is not big. Bob is blue. Bob is cold. Bob is nice. Bob is red. Dave is blue. Dave is cold. Dave is nice. Harry is not round. If something is big and not red then it is blue. If something is round then it is young. If Harry is nice and Harry is big then Harry is blue. Nice, blue things are round. All big things are round. Big, young things are not nice. If Bob is not blue then Bob is nice. If Dave is not blue then Dave is round.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is not big.
("Bob" "is" "big" "-")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Harry is not round.
("Harry" "is" "round" "-")
If something is big and not red then it is blue.
((("something" "is" "big" "+") ("something" "is" "red" "~")) -> ("something" "is" "blue" "+"))
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If Harry is nice and Harry is big then Harry is blue.
((("Harry" "is" "nice" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "blue" "+"))
Nice, blue things are round.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Big, young things are not nice.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "-"))
If Bob is not blue then Bob is nice.
((("Bob" "is" "blue" "~")) -> ("Bob" "is" "nice" "+"))
If Dave is not blue then Dave is round.
((("Dave" "is" "blue" "~")) -> ("Dave" "is" "round" "+"))
Dave is cold.
True
1
proof
[(triple10)]
("Dave" "is" "cold" "+")
triple10
Bob is not nice.
False
1
inv-proof
[(triple7)]
("Bob" "is" "nice" "-")
triple7
Dave is round.
True
3
proof
[(((triple11 triple9) -> rule4))]
("Dave" "is" "round" "+")
((triple11 triple9) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
3
inv-proof
[(((triple11 triple9) -> rule4))]
("Dave" "is" "round" "-")
((triple11 triple9) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
True
4
proof
[(((((triple11 triple9) -> rule4)) -> rule2))]
("Dave" "is" "young" "+")
((((triple11 triple9) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is not young.
False
4
inv-proof
[(((((triple11 triple9) -> rule4)) -> rule2))]
("Dave" "is" "young" "-")
((((triple11 triple9) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Anne is not nice.
True
5
proof
[(((triple1 ((((triple1) -> rule5)) -> rule2)) -> rule6))]
("Anne" "is" "nice" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is nice.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule5)) -> rule2)) -> rule6))]
("Anne" "is" "nice" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is red.[(triple3)] Bob is blue.[(triple5)] Bob is cold.[(triple6)] Bob is nice.[(triple7)] Bob is not big.[(triple4)] Bob is red.[(triple8)] Dave is blue.[(triple9)] Dave is cold.[(triple10)] Dave is nice.[(triple11)] Harry is not round.[(triple12)] @1: Anne is round.[(((triple1) -> rule5))] Bob is round.[(((triple7 triple5) -> rule4))] Dave is round.[(((triple11 triple9) -> rule4))] @2: Anne is young.[(((((triple1) -> rule5)) -> rule2))] Bob is young.[(((((triple7 triple5) -> rule4)) -> rule2))] Dave is young.[(((((triple11 triple9) -> rule4)) -> rule2))] @3: Anne is not nice.[(((triple1 ((((triple1) -> rule5)) -> rule2)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple5
Bob is cold.
("Bob" "is" "cold" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple7
Bob is not big.
("Bob" "is" "big" "-")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple8
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is cold.
("Dave" "is" "cold" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
Harry is not round.
("Harry" "is" "round" "-")
triple12
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple7 triple5) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple11 triple9) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple7 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple11 triple9) -> (rule4 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3