Bob is big. Dave is red. Dave is young. Fiona is blue. Harry is blue. Harry is kind. Harry is red. If someone is big then they are red. If someone is cold and not quiet then they are red. Cold, blue people are red. If someone is blue then they are big. If someone is red then they are young. If someone is kind then they are not cold. All kind people are not cold. If someone is young and blue then they are kind. If Fiona is kind then Fiona is blue.
Bob is big.
("Bob" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and not quiet then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "red" "+"))
Cold, blue people are red.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is blue then they are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is kind then they are not cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "-"))
All kind people are not cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "-"))
If someone is young and blue then they are kind.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Fiona is kind then Fiona is blue.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "blue" "+"))
Dave is red.
True
1
proof
[(triple2)]
("Dave" "is" "red" "+")
triple2
Dave is not young.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule5))]
("Dave" "is" "young" "-")
triple3
((triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is red.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "red" "+")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is cold.
False
2
inv-proof
[(((triple6) -> rule6) OR ((triple6) -> rule7) OR ((((((triple7) -> rule5) triple5) -> rule8)) -> rule6) OR ((((((triple7) -> rule5) triple5) -> rule8)) -> rule7) OR ((((((((((triple5) -> rule4)) -> rule1)) -> rule5) triple5) -> rule8)) -> rule6) OR ((((((((((triple5) -> rule4)) -> rule1)) -> rule5) triple5) -> rule8)) -> rule7))]
("Harry" "is" "cold" "+")
((triple6) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
((triple6) -> (rule7 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
((((((triple7) -> (rule5 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple7) -> (rule5 % int3)) triple5) -> (rule8 % int2))) -> (rule7 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((((((triple5) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5
((((((((((triple5) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple5) -> (rule8 % int2))) -> (rule7 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5
Fiona is red.
True
3
proof
[(((((triple4) -> rule4)) -> rule1))]
("Fiona" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not red.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule1))]
("Fiona" "is" "red" "-")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
True
4
proof
[(((((((triple4) -> rule4)) -> rule1)) -> rule5))]
("Fiona" "is" "young" "+")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not young.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule1)) -> rule5))]
("Fiona" "is" "young" "-")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is kind.
True
6
proof
[(((((((((triple4) -> rule4)) -> rule1)) -> rule5) triple4) -> rule8))]
("Fiona" "is" "kind" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is not kind.
False
6
inv-proof
[(((((((((triple4) -> rule4)) -> rule1)) -> rule5) triple4) -> rule8))]
("Fiona" "is" "kind" "-")
((((((((triple4) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is not cold.
True
7
proof
[(((((((((((triple4) -> rule4)) -> rule1)) -> rule5) triple4) -> rule8)) -> rule6) OR ((((((((((triple4) -> rule4)) -> rule1)) -> rule5) triple4) -> rule8)) -> rule7))]
("Fiona" "is" "cold" "-")
((((((((((triple4) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple4) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
((((((((((triple4) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple4) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
Fiona is cold.
False
7
inv-proof
[(((((((((((triple4) -> rule4)) -> rule1)) -> rule5) triple4) -> rule8)) -> rule6) OR ((((((((((triple4) -> rule4)) -> rule1)) -> rule5) triple4) -> rule8)) -> rule7))]
("Fiona" "is" "cold" "+")
((((((((((triple4) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple4) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
((((((((((triple4) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple4) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "kind" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "kind" "+")
Dave is not big.
Unknown
inv-rconc
[@1: Dave is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "big" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Dave is red.[(triple2)] Dave is young.[(triple3 OR ((triple2) -> rule5))] Fiona is blue.[(triple4)] Harry is blue.[(triple5)] Harry is kind.[(triple6 OR ((((triple7) -> rule5) triple5) -> rule8) OR ((((((((triple5) -> rule4)) -> rule1)) -> rule5) triple5) -> rule8))] Harry is red.[(triple7 OR ((((triple5) -> rule4)) -> rule1))] @1: Bob is red.[(((triple1) -> rule1))] Fiona is big.[(((triple4) -> rule4))] Harry is big.[(((triple5) -> rule4))] Harry is not cold.[(((triple6) -> rule6) OR ((triple6) -> rule7) OR ((((((triple7) -> rule5) triple5) -> rule8)) -> rule6) OR ((((((triple7) -> rule5) triple5) -> rule8)) -> rule7) OR ((((((((((triple5) -> rule4)) -> rule1)) -> rule5) triple5) -> rule8)) -> rule6) OR ((((((((((triple5) -> rule4)) -> rule1)) -> rule5) triple5) -> rule8)) -> rule7))] Harry is young.[(((triple7) -> rule5) OR ((((((triple5) -> rule4)) -> rule1)) -> rule5))] @2: Bob is young.[(((((triple1) -> rule1)) -> rule5))] Fiona is red.[(((((triple4) -> rule4)) -> rule1))] @3: Fiona is young.[(((((((triple4) -> rule4)) -> rule1)) -> rule5))] @4: Fiona is kind.[(((((((((triple4) -> rule4)) -> rule1)) -> rule5) triple4) -> rule8))] @5: Fiona is not cold.[(((((((((((triple4) -> rule4)) -> rule1)) -> rule5) triple4) -> rule8)) -> rule6) OR ((((((((((triple4) -> rule4)) -> rule1)) -> rule5) triple4) -> rule8)) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
((triple2) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Harry is blue.
("Harry" "is" "blue" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
((((triple7) -> (rule5 % int2)) triple5) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((((triple5) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple5) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is red.
("Harry" "is" "red" "+")
triple7
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple4) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple5) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((triple6) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
((triple6) -> (rule7 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
((((((triple7) -> (rule5 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple7) -> (rule5 % int3)) triple5) -> (rule8 % int2))) -> (rule7 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((((((triple5) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple5) -> (rule8 % int2))) -> (rule6 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5
((((((((((triple5) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple5) -> (rule8 % int2))) -> (rule7 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is big.
("Harry" "is" "big" "+")
int5
Harry is young.
("Harry" "is" "young" "+")
((triple7) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((((triple4) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) triple4) -> (rule8 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is red.
("Fiona" "is" "red" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Fiona is not cold.
("Fiona" "is" "cold" "-")
((((((((((triple4) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple4) -> (rule8 % int2))) -> (rule6 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
((((((((((triple4) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule5 % int3)) triple4) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is not cold.
("Fiona" "is" "cold" "-")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is red.
("Fiona" "is" "red" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5