Charlie is green. Fiona is kind. Fiona is smart. All green things are big. All big things are rough. Red, big things are green. All rough things are red. If Charlie is green and Charlie is rough then Charlie is smart. If Charlie is smart then Charlie is red.
Charlie is green.
("Charlie" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
All green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Red, big things are green.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If Charlie is green and Charlie is rough then Charlie is smart.
((("Charlie" "is" "green" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "smart" "+"))
If Charlie is smart then Charlie is red.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "red" "+"))
Fiona is kind.
True
1
proof
[(triple2)]
("Fiona" "is" "kind" "+")
triple2
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Charlie is big.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "big" "+")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "big" "-")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not rough.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "rough" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule5))]
("Charlie" "is" "smart" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not smart.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule5))]
("Charlie" "is" "smart" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Fiona is not green.
Unknown
inv-rconc
[@2: Fiona is green.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "green" "-")
Fiona is red.
Unknown
rconc
[@4: Fiona is red.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "big" "-")
Fiona is rough.
Unknown
rconc
[@3: Fiona is rough.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "rough" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is green.[(triple1)] Fiona is kind.[(triple2)] Fiona is smart.[(triple3)] @1: Charlie is big.[(((triple1) -> rule1))] @2: Charlie is rough.[(((((triple1) -> rule1)) -> rule2))] @3: Charlie is red.[(((((((triple1) -> rule1)) -> rule2)) -> rule4) OR ((((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule5)) -> rule6))] Charlie is smart.[(((triple1 ((((triple1) -> rule1)) -> rule2)) -> rule5))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple1 ((((triple1) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3