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