Charlie is big. Charlie is kind. Charlie is smart. Dave is red. Dave is rough. Erin is not big. Erin is blue. Erin is not red. Fiona is not big. Fiona is red. Smart things are red. If something is blue then it is not red. All red, rough things are kind. If something is kind and red then it is smart. Kind, rough things are smart. If something is red and kind then it is smart. If Dave is blue then Dave is rough. All rough, smart things are not round.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is not big.
("Erin" "is" "big" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not red.
("Erin" "is" "red" "-")
Fiona is not big.
("Fiona" "is" "big" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If something is blue then it is not red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "-"))
All red, rough things are kind.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is kind and red then it is smart.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Kind, rough things are smart.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is red and kind then it is smart.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
If Dave is blue then Dave is rough.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "rough" "+"))
All rough, smart things are not round.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
Dave is red.
True
1
proof
[(triple4)]
("Dave" "is" "red" "+")
triple4
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Dave is kind.
True
3
proof
[(((triple4 triple5) -> rule3))]
("Dave" "is" "kind" "+")
((triple4 triple5) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
3
inv-proof
[(((triple4 triple5) -> rule3))]
("Dave" "is" "kind" "-")
((triple4 triple5) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
True
5
proof
[(((triple4 ((triple4 triple5) -> rule3)) -> rule6) OR ((((triple4 triple5) -> rule3) triple4) -> rule4) OR ((((triple4 triple5) -> rule3) triple5) -> rule5))]
("Dave" "is" "smart" "+")
((triple4 ((triple4 triple5) -> (rule3 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple4 triple5) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple4 triple5) -> (rule3 % int2)) triple5) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not smart.
False
5
inv-proof
[(((triple4 ((triple4 triple5) -> rule3)) -> rule6) OR ((((triple4 triple5) -> rule3) triple4) -> rule4) OR ((((triple4 triple5) -> rule3) triple5) -> rule5))]
("Dave" "is" "smart" "-")
((triple4 ((triple4 triple5) -> (rule3 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple4 triple5) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple4 triple5) -> (rule3 % int2)) triple5) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not round.
True
7
proof
[(((triple5 ((triple4 ((triple4 triple5) -> rule3)) -> rule6)) -> rule8) OR ((triple5 ((((triple4 triple5) -> rule3) triple4) -> rule4)) -> rule8) OR ((triple5 ((((triple4 triple5) -> rule3) triple5) -> rule5)) -> rule8))]
("Dave" "is" "round" "-")
((triple5 ((triple4 ((triple4 triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple5 ((((triple4 triple5) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule8 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple5 ((((triple4 triple5) -> (rule3 % int3)) triple5) -> (rule5 % int2))) -> (rule8 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is round.
False
7
inv-proof
[(((triple5 ((triple4 ((triple4 triple5) -> rule3)) -> rule6)) -> rule8) OR ((triple5 ((((triple4 triple5) -> rule3) triple4) -> rule4)) -> rule8) OR ((triple5 ((((triple4 triple5) -> rule3) triple5) -> rule5)) -> rule8))]
("Dave" "is" "round" "+")
((triple5 ((triple4 ((triple4 triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple5 ((((triple4 triple5) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule8 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple5 ((((triple4 triple5) -> (rule3 % int3)) triple5) -> (rule5 % int2))) -> (rule8 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "smart" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "kind" "+")
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "kind" "-")
Fiona is smart.
Unknown
rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Fiona" "is" "smart" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Charlie is big.[(triple1)] Charlie is kind.[(triple2)] Charlie is smart.[(triple3)] Dave is red.[(triple4)] Dave is rough.[(triple5)] Erin is blue.[(triple7)] Erin is not big.[(triple6)] Erin is not red.[(triple8 OR ((triple7) -> rule2))] Fiona is not big.[(triple9)] Fiona is red.[(triple10)] @1: Charlie is red.[(((triple3) -> rule1))] Dave is kind.[(((triple4 triple5) -> rule3))] @2: Dave is smart.[(((triple4 ((triple4 triple5) -> rule3)) -> rule6) OR ((((triple4 triple5) -> rule3) triple4) -> rule4) OR ((((triple4 triple5) -> rule3) triple5) -> rule5))] @3: Dave is not round.[(((triple5 ((triple4 ((triple4 triple5) -> rule3)) -> rule6)) -> rule8) OR ((triple5 ((((triple4 triple5) -> rule3) triple4) -> rule4)) -> rule8) OR ((triple5 ((((triple4 triple5) -> rule3) triple5) -> rule5)) -> rule8))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is not big.
("Erin" "is" "big" "-")
triple6
Erin is not red.
("Erin" "is" "red" "-")
triple8
((triple7) -> (rule2 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Fiona is not big.
("Fiona" "is" "big" "-")
triple9
Fiona is red.
("Fiona" "is" "red" "+")
triple10
Charlie is red.
("Charlie" "is" "red" "+")
((triple3) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple4 triple5) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple4 ((triple4 triple5) -> (rule3 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple4 triple5) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple4 triple5) -> (rule3 % int2)) triple5) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
((triple5 ((triple4 ((triple4 triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple5 ((((triple4 triple5) -> (rule3 % int3)) triple4) -> (rule4 % int2))) -> (rule8 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
((triple5 ((((triple4 triple5) -> (rule3 % int3)) triple5) -> (rule5 % int2))) -> (rule8 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3