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