Anne is big. Anne is blue. Anne is kind. Anne is red. Anne is rough. Anne is round. Anne is white. Bob is big. Bob is blue. Bob is rough. Bob is not white. Dave is not red. Dave is not rough. Dave is round. Dave is white. Fiona is blue. Big, round things are kind. All big, blue things are kind. Kind things are round. If something is kind and not blue then it is white. All blue things are big. All big, white things are 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 round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is not white.
("Bob" "is" "white" "-")
Dave is not red.
("Dave" "is" "red" "-")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Big, round things are kind.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
All big, blue things are kind.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is kind and not blue then it is white.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "is" "white" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
All big, white things are red.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
Anne is white.
True
1
proof
[(triple7)]
("Anne" "is" "white" "+")
triple7
Bob is not big.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule5))]
("Bob" "is" "big" "-")
triple8
((triple9) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Fiona is big.
True
2
proof
[(((triple16) -> rule5))]
("Fiona" "is" "big" "+")
((triple16) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is not big.
False
2
inv-proof
[(((triple16) -> rule5))]
("Fiona" "is" "big" "-")
((triple16) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Bob is round.
True
4
proof
[(((((triple8 triple9) -> rule2)) -> rule3) OR ((((((triple9) -> rule5) triple9) -> rule2)) -> rule3))]
("Bob" "is" "round" "+")
((((triple8 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple9) -> (rule5 % int3)) triple9) -> (rule2 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not round.
False
4
inv-proof
[(((((triple8 triple9) -> rule2)) -> rule3) OR ((((((triple9) -> rule5) triple9) -> rule2)) -> rule3))]
("Bob" "is" "round" "-")
((((triple8 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple9) -> (rule5 % int3)) triple9) -> (rule2 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Fiona is round.
True
5
proof
[(((((((triple16) -> rule5) triple16) -> rule2)) -> rule3))]
("Fiona" "is" "round" "+")
((((((triple16) -> (rule5 % int3)) triple16) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not round.
False
5
inv-proof
[(((((((triple16) -> rule5) triple16) -> rule2)) -> rule3))]
("Fiona" "is" "round" "-")
((((((triple16) -> (rule5 % int3)) triple16) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "white" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "red" "+")
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is kind.
Unknown
rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Dave" "is" "kind" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is big.[(triple1 OR ((triple2) -> rule5))] Anne is blue.[(triple2)] Anne is kind.[(triple3 OR ((triple1 triple2) -> rule2) OR ((triple1 triple6) -> rule1) OR ((((triple2) -> rule5) triple2) -> rule2) OR ((((triple2) -> rule5) triple6) -> rule1))] Anne is red.[(triple4 OR ((triple1 triple7) -> rule6) OR ((((triple2) -> rule5) triple7) -> rule6))] Anne is rough.[(triple5)] Anne is round.[(triple6 OR ((triple3) -> rule3) OR ((((triple1 triple2) -> rule2)) -> rule3) OR ((((((triple2) -> rule5) triple2) -> rule2)) -> rule3))] Anne is white.[(triple7)] Bob is big.[(triple8 OR ((triple9) -> rule5))] Bob is blue.[(triple9)] Bob is not white.[(triple11)] Bob is rough.[(triple10)] Dave is not red.[(triple12)] Dave is not rough.[(triple13)] Dave is round.[(triple14)] Dave is white.[(triple15)] Fiona is blue.[(triple16)] @1: Bob is kind.[(((triple8 triple9) -> rule2) OR ((((triple9) -> rule5) triple9) -> rule2))] Fiona is big.[(((triple16) -> rule5))] @2: Bob is round.[(((((triple8 triple9) -> rule2)) -> rule3) OR ((((((triple9) -> rule5) triple9) -> rule2)) -> rule3))] Fiona is kind.[(((((triple16) -> rule5) triple16) -> rule2))] @3: Fiona is round.[(((((((triple16) -> rule5) triple16) -> rule2)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple1 triple2) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 triple6) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
((((triple2) -> (rule5 % int2)) triple6) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple1 triple7) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((triple2) -> (rule5 % int2)) triple7) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple3) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple1 triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((((triple2) -> (rule5 % int3)) triple2) -> (rule2 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
triple7
Bob is big.
("Bob" "is" "big" "+")
triple8
((triple9) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple9
Bob is not white.
("Bob" "is" "white" "-")
triple11
Bob is rough.
("Bob" "is" "rough" "+")
triple10
Dave is not red.
("Dave" "is" "red" "-")
triple12
Dave is not rough.
("Dave" "is" "rough" "-")
triple13
Dave is round.
("Dave" "is" "round" "+")
triple14
Dave is white.
("Dave" "is" "white" "+")
triple15
Fiona is blue.
("Fiona" "is" "blue" "+")
triple16
Bob is kind.
("Bob" "is" "kind" "+")
((triple8 triple9) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple9) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((triple16) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple8 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple9) -> (rule5 % int3)) triple9) -> (rule2 % int2))) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple16) -> (rule5 % int2)) triple16) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((((triple16) -> (rule5 % int3)) triple16) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3