Bob is cold. Charlie is furry. Charlie is white. Fiona is not big. Fiona is green. Gary is smart. Gary is white. If Fiona is quiet and Fiona is furry then Fiona is green. If Fiona is smart then Fiona is white. Big people are quiet. All quiet people are smart. If someone is smart and white then they are not cold. Furry people are green. Smart people are green. If Charlie is green then Charlie is big.
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
If Fiona is quiet and Fiona is furry then Fiona is green.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "green" "+"))
If Fiona is smart then Fiona is white.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "white" "+"))
Big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and white then they are not cold.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "-"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If Charlie is green then Charlie is big.
((("Charlie" "is" "green" "+")) -> ("Charlie" "is" "big" "+"))
Gary is smart.
True
1
proof
[(triple6)]
("Gary" "is" "smart" "+")
triple6
Gary is not smart.
False
1
inv-proof
[(triple6)]
("Gary" "is" "smart" "-")
triple6
Gary is green.
True
2
proof
[(((triple6) -> rule7))]
("Gary" "is" "green" "+")
((triple6) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
False
3
inv-proof
[(((triple6 triple7) -> rule5))]
("Gary" "is" "cold" "+")
((triple6 triple7) -> (rule5 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Charlie is big.
True
3
proof
[(((((triple2) -> rule6)) -> rule8))]
("Charlie" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule8))]
("Charlie" "is" "big" "-")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
True
4
proof
[(((((((triple2) -> rule6)) -> rule8)) -> rule3))]
("Charlie" "is" "quiet" "+")
((((((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is not quiet.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule8)) -> rule3))]
("Charlie" "is" "quiet" "-")
((((((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is smart.
True
5
proof
[(((((((((triple2) -> rule6)) -> rule8)) -> rule3)) -> rule4))]
("Charlie" "is" "smart" "+")
((((((((triple2) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is not smart.
False
5
inv-proof
[(((((((((triple2) -> rule6)) -> rule8)) -> rule3)) -> rule4))]
("Charlie" "is" "smart" "-")
((((((((triple2) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is not cold.
True
7
proof
[(((((((((((triple2) -> rule6)) -> rule8)) -> rule3)) -> rule4) triple3) -> rule5))]
("Charlie" "is" "cold" "-")
((((((((((triple2) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
int5
Charlie is cold.
False
7
inv-proof
[(((((((((((triple2) -> rule6)) -> rule8)) -> rule3)) -> rule4) triple3) -> rule5))]
("Charlie" "is" "cold" "+")
((((((((((triple2) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
int5
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is smart.
Unknown
rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Bob" "is" "smart" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Gary is quiet.
Unknown
rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "+")
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is white.
Unknown
rconc
[@3: Fiona is white.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule3 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Charlie is furry.[(triple2)] Charlie is white.[(triple3)] Fiona is green.[(triple5)] Fiona is not big.[(triple4)] Gary is smart.[(triple6)] Gary is white.[(triple7)] @1: Charlie is green.[(((triple2) -> rule6))] Gary is green.[(((triple6) -> rule7))] Gary is not cold.[(((triple6 triple7) -> rule5))] @2: Charlie is big.[(((((triple2) -> rule6)) -> rule8))] @3: Charlie is quiet.[(((((((triple2) -> rule6)) -> rule8)) -> rule3))] @4: Charlie is smart.[(((((((((triple2) -> rule6)) -> rule8)) -> rule3)) -> rule4))] @5: Charlie is not cold.[(((((((((((triple2) -> rule6)) -> rule8)) -> rule3)) -> rule4) triple3) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Fiona is not big.
("Fiona" "is" "big" "-")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple6) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not cold.
("Gary" "is" "cold" "-")
((triple6 triple7) -> (rule5 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple2) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((((triple2) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is not cold.
("Charlie" "is" "cold" "-")
((((((((((triple2) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) triple3) -> (rule5 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
int5