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