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