Charlie is blue. Fiona is rough. Harry is rough. If Charlie is blue then Charlie is rough. If something is rough then it is white. If Fiona is blue and Fiona is not white then Fiona is round. If something is blue and not rough then it is green. White things are green. If something is round and not green then it is quiet.
Charlie is blue.
("Charlie" "is" "blue" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Charlie is blue then Charlie is rough.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "rough" "+"))
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Fiona is blue and Fiona is not white then Fiona is round.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "white" "~")) -> ("Fiona" "is" "round" "+"))
If something is blue and not rough then it is green.
((("something" "is" "blue" "+") ("something" "is" "rough" "~")) -> ("something" "is" "green" "+"))
White things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is round and not green then it is quiet.
((("something" "is" "round" "+") ("something" "is" "green" "~")) -> ("something" "is" "quiet" "+"))
Fiona is rough.
True
1
proof
[(triple2)]
("Fiona" "is" "rough" "+")
triple2
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is rough.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "white" "-")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
True
3
proof
[(((((triple3) -> rule2)) -> rule5))]
("Harry" "is" "green" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Fiona is not green.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("Fiona" "is" "green" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Charlie is green.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule5))]
("Charlie" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not green.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule5))]
("Charlie" "is" "green" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "quiet" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "round" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is blue.[(triple1)] Fiona is rough.[(triple2)] Harry is rough.[(triple3)] @1: Charlie is rough.[(((triple1) -> rule1))] Fiona is white.[(((triple2) -> rule2))] Harry is white.[(((triple3) -> rule2))] @2: Charlie is white.[(((((triple1) -> rule1)) -> rule2))] Fiona is green.[(((((triple2) -> rule2)) -> rule5))] Harry is green.[(((((triple3) -> rule2)) -> rule5))] @3: Charlie is green.[(((((((triple1) -> rule1)) -> rule2)) -> rule5))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple2) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple3) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3