Charlie is white. Dave is blue. Dave is furry. Dave is red. Dave is rough. Dave is round. Dave is smart. Dave is white. Erin is red. Erin is smart. All smart, round people are blue. If someone is smart then they are round. All blue people are rough.
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
All smart, round people are blue.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart then they are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Erin is red.
True
1
proof
[(triple9)]
("Erin" "is" "red" "+")
triple9
Dave is not red.
False
1
inv-proof
[(triple4)]
("Dave" "is" "red" "-")
triple4
Erin is round.
True
2
proof
[(((triple10) -> rule2))]
("Erin" "is" "round" "+")
((triple10) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple10) -> rule2))]
("Erin" "is" "round" "-")
((triple10) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is blue.
True
4
proof
[(((triple10 ((triple10) -> rule2)) -> rule1))]
("Erin" "is" "blue" "+")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not blue.
False
4
inv-proof
[(((triple10 ((triple10) -> rule2)) -> rule1))]
("Erin" "is" "blue" "-")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
True
5
proof
[(((((triple10 ((triple10) -> rule2)) -> rule1)) -> rule3))]
("Erin" "is" "rough" "+")
((((triple10 ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not rough.
False
5
inv-proof
[(((((triple10 ((triple10) -> rule2)) -> rule1)) -> rule3))]
("Erin" "is" "rough" "-")
((((triple10 ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not rough.
Unknown
inv-rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is white.[(triple1)] Dave is blue.[(triple2 OR ((triple7 triple6) -> rule1) OR ((triple7 ((triple7) -> rule2)) -> rule1))] Dave is furry.[(triple3)] Dave is red.[(triple4)] Dave is rough.[(triple5 OR ((triple2) -> rule3) OR ((((triple7 triple6) -> rule1)) -> rule3) OR ((((triple7 ((triple7) -> rule2)) -> rule1)) -> rule3))] Dave is round.[(triple6 OR ((triple7) -> rule2))] Dave is smart.[(triple7)] Dave is white.[(triple8)] Erin is red.[(triple9)] Erin is smart.[(triple10)] @1: Erin is round.[(((triple10) -> rule2))] @2: Erin is blue.[(((triple10 ((triple10) -> rule2)) -> rule1))] @3: Erin is rough.[(((((triple10 ((triple10) -> rule2)) -> rule1)) -> rule3))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
((triple7 triple6) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((triple7 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple2) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple7 triple6) -> (rule1 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple7 ((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
triple6
((triple7) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Dave is white.
("Dave" "is" "white" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
Erin is smart.
("Erin" "is" "smart" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
((triple10) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple10 ((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3