Charlie is red. Erin is rough. Fiona is white. All young, red things are rough. Round, smart things are rough. Red, kind things are young. All kind things are white. Rough, kind things are red. If something is red then it is white. If something is rough then it is kind. All red things are young.
Charlie is red.
("Charlie" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
All young, red things are rough.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
Round, smart things are rough.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
Red, kind things are young.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Rough, kind things are red.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Charlie is red.
True
1
proof
[(triple1)]
("Charlie" "is" "red" "+")
triple1
Fiona is not white.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "white" "-")
triple3
Charlie is white.
True
2
proof
[(((triple1) -> rule6) OR ((((((((triple1) -> rule8) triple1) -> rule1)) -> rule7)) -> rule4))]
("Charlie" "is" "white" "+")
((triple1) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((((((triple1) -> (rule8 % int4)) triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Erin is not kind.
False
2
inv-proof
[(((triple2) -> rule7))]
("Erin" "is" "kind" "-")
((triple2) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Fiona is not red.
Unknown
inv-rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is kind.
Unknown
rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule5 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is red.[(triple1)] Erin is rough.[(triple2)] Fiona is white.[(triple3)] @1: Charlie is white.[(((triple1) -> rule6) OR ((((((((triple1) -> rule8) triple1) -> rule1)) -> rule7)) -> rule4))] Charlie is young.[(((triple1) -> rule8))] Erin is kind.[(((triple2) -> rule7))] @2: Charlie is rough.[(((((triple1) -> rule8) triple1) -> rule1))] Erin is red.[(((triple2 ((triple2) -> rule7)) -> rule5))] Erin is white.[(((((triple2) -> rule7)) -> rule4) OR ((((triple2 ((triple2) -> rule7)) -> rule5)) -> rule6))] @3: Charlie is kind.[(((((((triple1) -> rule8) triple1) -> rule1)) -> rule7))] Erin is young.[(((((triple2 ((triple2) -> rule7)) -> rule5)) -> rule8) OR ((((triple2 ((triple2) -> rule7)) -> rule5) ((triple2) -> rule7)) -> rule3))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((((((triple1) -> (rule8 % int4)) triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple2) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((triple2 ((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule5 % int2)) ((triple2) -> (rule7 % int3))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3