Bob is big. Bob is cold. Bob is smart. All big things are round. If something is rough and quiet then it is big. If Bob is cold then Bob is rough. Quiet things are big. If something is young and rough then it is cold. If something is round then it is cold. If Bob is smart and Bob is rough then Bob is young. All quiet things are cold.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is smart.
("Bob" "is" "smart" "+")
All big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something is rough and quiet then it is big.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If Bob is cold then Bob is rough.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "rough" "+"))
Quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is young and rough then it is cold.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is round then it is cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If Bob is smart and Bob is rough then Bob is young.
((("Bob" "is" "smart" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "young" "+"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Bob is smart.
True
1
proof
[(triple3)]
("Bob" "is" "smart" "+")
triple3
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is rough.
True
2
proof
[(((triple2) -> rule3) OR ((((((triple1) -> rule1)) -> rule6)) -> rule3))]
("Bob" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "round" "-")
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
True
4
proof
[(((triple3 ((triple2) -> rule3)) -> rule7) OR ((triple3 ((((((triple1) -> rule1)) -> rule6)) -> rule3)) -> rule7))]
("Bob" "is" "young" "+")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((triple3 ((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is not young.
False
4
inv-proof
[(((triple3 ((triple2) -> rule3)) -> rule7) OR ((triple3 ((((((triple1) -> rule1)) -> rule6)) -> rule3)) -> rule7))]
("Bob" "is" "young" "-")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((triple3 ((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
@0: Bob is big.[(triple1)] Bob is cold.[(triple2 OR ((((triple1) -> rule1)) -> rule6))] Bob is smart.[(triple3)] @1: Bob is rough.[(((triple2) -> rule3) OR ((((((triple1) -> rule1)) -> rule6)) -> rule3))] Bob is round.[(((triple1) -> rule1))] @2: Bob is young.[(((triple3 ((triple2) -> rule3)) -> rule7) OR ((triple3 ((((((triple1) -> rule1)) -> rule6)) -> rule3)) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple3 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((triple3 ((((((triple1) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4