Charlie is green. Charlie is smart. Erin is big. Erin is rough. Erin is white. Erin is young. Fiona is big. Fiona is green. Fiona is quiet. Fiona is rough. Fiona is young. Gary is rough. Smart, green things are big. All rough things are white. If something is green and smart then it is white. All quiet things are green. If something is rough then it is young. If Charlie is white and Charlie is young then Charlie is green. If Gary is quiet and Gary is smart then Gary is rough. Young things are big.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Smart, green things are big.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If something is green and smart then it is white.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If Charlie is white and Charlie is young then Charlie is green.
((("Charlie" "is" "white" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "green" "+"))
If Gary is quiet and Gary is smart then Gary is rough.
((("Gary" "is" "quiet" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "rough" "+"))
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Erin is young.
True
1
proof
[(triple6 OR ((triple4) -> rule5))]
("Erin" "is" "young" "+")
triple6
((triple4) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is not quiet.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "quiet" "-")
triple9
Fiona is white.
True
2
proof
[(((triple10) -> rule2))]
("Fiona" "is" "white" "+")
((triple10) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Charlie is not white.
False
3
inv-proof
[(((triple1 triple2) -> rule3))]
("Charlie" "is" "white" "-")
((triple1 triple2) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is big.
True
3
proof
[(((((triple12) -> rule5)) -> rule8))]
("Gary" "is" "big" "+")
((((triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not big.
False
3
inv-proof
[(((((triple12) -> rule5)) -> rule8))]
("Gary" "is" "big" "-")
((((triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "green" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "young" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Charlie is green.[(triple1)] Charlie is smart.[(triple2)] Erin is big.[(triple3 OR ((triple6) -> rule8) OR ((((triple4) -> rule5)) -> rule8))] Erin is rough.[(triple4)] Erin is white.[(triple5 OR ((triple4) -> rule2))] Erin is young.[(triple6 OR ((triple4) -> rule5))] Fiona is big.[(triple7 OR ((triple11) -> rule8) OR ((((triple10) -> rule5)) -> rule8))] Fiona is green.[(triple8 OR ((triple9) -> rule4))] Fiona is quiet.[(triple9)] Fiona is rough.[(triple10)] Fiona is young.[(triple11 OR ((triple10) -> rule5))] Gary is rough.[(triple12)] @1: Charlie is big.[(((triple2 triple1) -> rule1))] Charlie is white.[(((triple1 triple2) -> rule3))] Fiona is white.[(((triple10) -> rule2))] Gary is white.[(((triple12) -> rule2))] Gary is young.[(((triple12) -> rule5))] @2: Gary is big.[(((((triple12) -> rule5)) -> rule8))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
((triple6) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is white.
("Erin" "is" "white" "+")
triple5
((triple4) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple6
((triple4) -> (rule5 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple7
((triple11) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule8 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
triple8
((triple9) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
Fiona is young.
("Fiona" "is" "young" "+")
triple11
((triple10) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Charlie is big.
("Charlie" "is" "big" "+")
((triple2 triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple1 triple2) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple10) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple12) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple12) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple12) -> (rule5 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2