Bob is cold. Bob is furry. Bob is red. Charlie is cold. Charlie is green. Charlie is red. Fiona is cold. Fiona is furry. Fiona is green. Fiona is quiet. Fiona is red. Fiona is round. Harry is cold. Harry is furry. Harry is green. Harry is round. Round, green people are nice. All quiet people are red. Cold, nice people are furry. Round, nice people are quiet. If Bob is quiet then Bob is green. If Fiona is red then Fiona is round.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is round.
("Harry" "is" "round" "+")
Round, green people are nice.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
All quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Cold, nice people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Round, nice people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is quiet then Bob is green.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "green" "+"))
If Fiona is red then Fiona is round.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "round" "+"))
Fiona is red.
True
1
proof
[(triple11 OR ((triple10) -> rule2) OR ((((triple12 ((triple12 triple9) -> rule1)) -> rule4)) -> rule2))]
("Fiona" "is" "red" "+")
triple11
((triple10) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple12 ((triple12 triple9) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is not quiet.
False
1
inv-proof
[(triple10 OR ((triple12 ((triple12 triple9) -> rule1)) -> rule4) OR ((((triple11) -> rule6) ((triple12 triple9) -> rule1)) -> rule4) OR ((triple12 ((((triple11) -> rule6) triple9) -> rule1)) -> rule4) OR ((((triple11) -> rule6) ((((triple11) -> rule6) triple9) -> rule1)) -> rule4))]
("Fiona" "is" "quiet" "-")
triple10
((triple12 ((triple12 triple9) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple11) -> (rule6 % int3)) ((triple12 triple9) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((triple12 ((((triple11) -> (rule6 % int3)) triple9) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((triple11) -> (rule6 % int3)) ((((triple11) -> (rule6 % int3)) triple9) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Harry is nice.
True
3
proof
[(((triple16 triple15) -> rule1))]
("Harry" "is" "nice" "+")
((triple16 triple15) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Fiona is not nice.
False
3
inv-proof
[(((triple12 triple9) -> rule1) OR ((((triple11) -> rule6) triple9) -> rule1) OR ((((((triple10) -> rule2)) -> rule6) triple9) -> rule1))]
("Fiona" "is" "nice" "-")
((triple12 triple9) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple11) -> (rule6 % int2)) triple9) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule6 % int2)) triple9) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Harry is quiet.
True
5
proof
[(((triple16 ((triple16 triple15) -> rule1)) -> rule4))]
("Harry" "is" "quiet" "+")
((triple16 ((triple16 triple15) -> (rule1 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not quiet.
False
5
inv-proof
[(((triple16 ((triple16 triple15) -> rule1)) -> rule4))]
("Harry" "is" "quiet" "-")
((triple16 ((triple16 triple15) -> (rule1 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
True
6
proof
[(((((triple16 ((triple16 triple15) -> rule1)) -> rule4)) -> rule2))]
("Harry" "is" "red" "+")
((((triple16 ((triple16 triple15) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is not red.
False
6
inv-proof
[(((((triple16 ((triple16 triple15) -> rule1)) -> rule4)) -> rule2))]
("Harry" "is" "red" "-")
((((triple16 ((triple16 triple15) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Bob is cold.[(triple1)] Bob is furry.[(triple2)] Bob is red.[(triple3)] Charlie is cold.[(triple4)] Charlie is green.[(triple5)] Charlie is red.[(triple6)] Fiona is cold.[(triple7)] Fiona is furry.[(triple8 OR ((triple7 ((triple12 triple9) -> rule1)) -> rule3) OR ((triple7 ((((triple11) -> rule6) triple9) -> rule1)) -> rule3) OR ((triple7 ((((((triple10) -> rule2)) -> rule6) triple9) -> rule1)) -> rule3))] Fiona is green.[(triple9)] Fiona is quiet.[(triple10 OR ((triple12 ((triple12 triple9) -> rule1)) -> rule4) OR ((((triple11) -> rule6) ((triple12 triple9) -> rule1)) -> rule4) OR ((triple12 ((((triple11) -> rule6) triple9) -> rule1)) -> rule4) OR ((((triple11) -> rule6) ((((triple11) -> rule6) triple9) -> rule1)) -> rule4))] Fiona is red.[(triple11 OR ((triple10) -> rule2) OR ((((triple12 ((triple12 triple9) -> rule1)) -> rule4)) -> rule2))] Fiona is round.[(triple12 OR ((triple11) -> rule6) OR ((((triple10) -> rule2)) -> rule6))] Harry is cold.[(triple13)] Harry is furry.[(triple14 OR ((triple13 ((triple16 triple15) -> rule1)) -> rule3))] Harry is green.[(triple15)] Harry is round.[(triple16)] @1: Fiona is nice.[(((triple12 triple9) -> rule1) OR ((((triple11) -> rule6) triple9) -> rule1) OR ((((((triple10) -> rule2)) -> rule6) triple9) -> rule1))] Harry is nice.[(((triple16 triple15) -> rule1))] @2: Harry is quiet.[(((triple16 ((triple16 triple15) -> rule1)) -> rule4))] @3: Harry is red.[(((((triple16 ((triple16 triple15) -> rule1)) -> rule4)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
((triple7 ((triple12 triple9) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((triple7 ((((triple11) -> (rule6 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((triple7 ((((((triple10) -> (rule2 % int4))) -> (rule6 % int3)) triple9) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple10
((triple12 ((triple12 triple9) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
((((triple11) -> (rule6 % int3)) ((triple12 triple9) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((triple12 ((((triple11) -> (rule6 % int3)) triple9) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
((((triple11) -> (rule6 % int3)) ((((triple11) -> (rule6 % int3)) triple9) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
triple11
((triple10) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((((triple12 ((triple12 triple9) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
int3
Fiona is round.
("Fiona" "is" "round" "+")
triple12
((triple11) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is furry.
("Harry" "is" "furry" "+")
triple14
((triple13 ((triple16 triple15) -> (rule1 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple15
Harry is round.
("Harry" "is" "round" "+")
triple16
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple12 triple9) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
((((triple11) -> (rule6 % int2)) triple9) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule6 % int2)) triple9) -> (rule1 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((triple16 triple15) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple16 ((triple16 triple15) -> (rule1 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple16 ((triple16 triple15) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3