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