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