Charlie is red. Erin is round. Harry is round. If someone is red then they are smart. All green, blue people are smart. Blue people are red. Red people are white. All round, green people are blue. Round people are blue.
Charlie is red.
("Charlie" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
All green, blue people are smart.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
All round, green people are blue.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Harry is round.
True
1
proof
[(triple3)]
("Harry" "is" "round" "+")
triple3
Charlie is not red.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "red" "-")
triple1
Erin is blue.
True
2
proof
[(((triple2) -> rule6))]
("Erin" "is" "blue" "+")
((triple2) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple3) -> rule6))]
("Harry" "is" "blue" "-")
((triple3) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("Harry" "is" "red" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not red.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule3))]
("Harry" "is" "red" "-")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Erin is white.
True
4
proof
[(((((((triple2) -> rule6)) -> rule3)) -> rule4))]
("Erin" "is" "white" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Harry is not white.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule3)) -> rule4))]
("Harry" "is" "white" "-")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Charlie is red.[(triple1)] Erin is round.[(triple2)] Harry is round.[(triple3)] @1: Charlie is smart.[(((triple1) -> rule1))] Charlie is white.[(((triple1) -> rule4))] Erin is blue.[(((triple2) -> rule6))] Harry is blue.[(((triple3) -> rule6))] @2: Erin is red.[(((((triple2) -> rule6)) -> rule3))] Harry is red.[(((((triple3) -> rule6)) -> rule3))] @3: Erin is smart.[(((((((triple2) -> rule6)) -> rule3)) -> rule1))] Erin is white.[(((((((triple2) -> rule6)) -> rule3)) -> rule4))] Harry is smart.[(((((((triple3) -> rule6)) -> rule3)) -> rule1))] Harry is white.[(((((((triple3) -> rule6)) -> rule3)) -> rule4))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((((triple3) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3