Charlie is white. Fiona is white. Harry is not big. If Charlie is blue then Charlie is smart. All green, young people are quiet. If someone is smart then they are not blue. If someone is white and green then they are big. If Fiona is quiet then Fiona is white. If someone is white then they are green.
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is not big.
("Harry" "is" "big" "-")
If Charlie is blue then Charlie is smart.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "smart" "+"))
All green, young people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart then they are not blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "-"))
If someone is white and green then they are big.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If Fiona is quiet then Fiona is white.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "white" "+"))
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Harry is not big.
True
1
proof
[(triple3)]
("Harry" "is" "big" "-")
triple3
Harry is big.
False
1
inv-proof
[(triple3)]
("Harry" "is" "big" "+")
triple3
Charlie is green.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "green" "+")
((triple1) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "green" "-")
((triple1) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
True
4
proof
[(((triple1 ((triple1) -> rule6)) -> rule4))]
("Charlie" "is" "big" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Fiona is not big.
False
4
inv-proof
[(((triple2 ((triple2) -> rule6)) -> rule4))]
("Fiona" "is" "big" "-")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "green" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "quiet" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Charlie is white.[(triple1)] Fiona is white.[(triple2)] Harry is not big.[(triple3)] @1: Charlie is green.[(((triple1) -> rule6))] Fiona is green.[(((triple2) -> rule6))] @2: Charlie is big.[(((triple1 ((triple1) -> rule6)) -> rule4))] Fiona is big.[(((triple2 ((triple2) -> rule6)) -> rule4))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Fiona is white.
("Fiona" "is" "white" "+")
triple2
Harry is not big.
("Harry" "is" "big" "-")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple2) -> (rule6 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2