Charlie is green. Charlie is rough. Harry is cold. All green things are rough. All blue things are rough. All cold things are young. All green things are quiet. If something is young then it is quiet. Green things are quiet. Blue things are cold. Young, quiet things are green.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is young then it is quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Young, quiet things are green.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Harry is cold.
True
1
proof
[(triple3)]
("Harry" "is" "cold" "+")
triple3
Charlie is not rough.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule1))]
("Charlie" "is" "rough" "-")
triple2
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
True
2
proof
[(((triple1) -> rule4) OR ((triple1) -> rule6))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple1) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "young" "-")
((triple3) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple3) -> rule3)) -> rule5))]
("Harry" "is" "quiet" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule5))]
("Harry" "is" "quiet" "-")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
True
6
proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule8))]
("Harry" "is" "green" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not green.
False
6
inv-proof
[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule8))]
("Harry" "is" "green" "-")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Charlie is not young.
Unknown
inv-rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "cold" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is green.[(triple1)] Charlie is rough.[(triple2 OR ((triple1) -> rule1))] Harry is cold.[(triple3)] @1: Charlie is quiet.[(((triple1) -> rule4) OR ((triple1) -> rule6))] Harry is young.[(((triple3) -> rule3))] @2: Harry is quiet.[(((((triple3) -> rule3)) -> rule5))] @3: Harry is green.[(((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule8))] @4: Harry is rough.[(((((((triple3) -> rule3) ((((triple3) -> rule3)) -> rule5)) -> rule8)) -> rule1))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple1) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple3) -> (rule3 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple3) -> (rule3 % int3)) ((((triple3) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple3) -> (rule3 % int4)) ((((triple3) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4