Charlie is young. Dave is big. Dave is cold. Dave is furry. Fiona is cold. Fiona is not young. Gary is young. All smart people are white. If someone is furry then they are white. If Fiona is not smart and Fiona is not young then Fiona is red. If someone is cold and not young then they are furry. If someone is cold then they are furry. If someone is white and cold then they are not red. If Fiona is smart and Fiona is white then Fiona is not big. If Charlie is white then Charlie is furry.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
Gary is young.
("Gary" "is" "young" "+")
All smart people are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If someone is furry then they are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If Fiona is not smart and Fiona is not young then Fiona is red.
((("Fiona" "is" "smart" "~") ("Fiona" "is" "young" "~")) -> ("Fiona" "is" "red" "+"))
If someone is cold and not young then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "furry" "+"))
If someone is cold then they are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is white and cold then they are not red.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "-"))
If Fiona is smart and Fiona is white then Fiona is not big.
((("Fiona" "is" "smart" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "big" "-"))
If Charlie is white then Charlie is furry.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "furry" "+"))
Charlie is young.
True
1
proof
[(triple1)]
("Charlie" "is" "young" "+")
triple1
Fiona is young.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "young" "+")
triple6
Dave is white.
True
2
proof
[(((triple4) -> rule2) OR ((((triple3) -> rule5)) -> rule2))]
("Dave" "is" "white" "+")
((triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Fiona is not furry.
False
2
inv-proof
[(((triple5) -> rule5) OR ((triple5 triple6) -> rule4))]
("Fiona" "is" "furry" "-")
((triple5) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple5 triple6) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Dave is not red.
True
4
proof
[(((((triple4) -> rule2) triple3) -> rule6) OR ((((((triple3) -> rule5)) -> rule2) triple3) -> rule6))]
("Dave" "is" "red" "-")
((((triple4) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is red.
False
4
inv-proof
[(((((triple4) -> rule2) triple3) -> rule6) OR ((((((triple3) -> rule5)) -> rule2) triple3) -> rule6))]
("Dave" "is" "red" "+")
((((triple4) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Fiona is not red.
True
5
proof
[(((((((triple5) -> rule5)) -> rule2) triple5) -> rule6) OR ((((((triple5 triple6) -> rule4)) -> rule2) triple5) -> rule6))]
("Fiona" "is" "red" "-")
((((((triple5) -> (rule5 % int3))) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple5 triple6) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Fiona is red.
False
5
inv-proof
[(((((((triple5) -> rule5)) -> rule2) triple5) -> rule6) OR ((((((triple5 triple6) -> rule4)) -> rule2) triple5) -> rule6))]
("Fiona" "is" "red" "+")
((((((triple5) -> (rule5 % int3))) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple5 triple6) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@3: Charlie is white.[CWA. Example of deepest failure = (rule2 <- rule8 <- rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Gary is furry.
Unknown
rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "furry" "+")
Charlie is not furry.
Unknown
inv-rconc
[@3: Charlie is furry.[CWA. Example of deepest failure = (rule8 <- rule2 <- rule4 <- FAIL)]]
("Charlie" "is" "furry" "-")
Gary is white.
Unknown
rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Charlie is young.[(triple1)] Dave is big.[(triple2)] Dave is cold.[(triple3)] Dave is furry.[(triple4 OR ((triple3) -> rule5))] Fiona is cold.[(triple5)] Fiona is not young.[(triple6)] Gary is young.[(triple7)] @1: Dave is white.[(((triple4) -> rule2) OR ((((triple3) -> rule5)) -> rule2))] Fiona is furry.[(((triple5) -> rule5) OR ((triple5 triple6) -> rule4))] @2: Dave is not red.[(((((triple4) -> rule2) triple3) -> rule6) OR ((((((triple3) -> rule5)) -> rule2) triple3) -> rule6))] Fiona is white.[(((((triple5) -> rule5)) -> rule2) OR ((((triple5 triple6) -> rule4)) -> rule2))] @3: Fiona is not red.[(((((((triple5) -> rule5)) -> rule2) triple5) -> rule6) OR ((((((triple5 triple6) -> rule4)) -> rule2) triple5) -> rule6))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
((triple3) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple5
Fiona is not young.
("Fiona" "is" "young" "-")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
((triple4) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple5) -> (rule5 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
((triple5 triple6) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Dave is not red.
("Dave" "is" "red" "-")
((((triple4) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Fiona is white.
("Fiona" "is" "white" "+")
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
((((triple5 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is not red.
("Fiona" "is" "red" "-")
((((((triple5) -> (rule5 % int3))) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3
((((((triple5 triple6) -> (rule4 % int3))) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
int3