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