Bob is big. Bob is not cold. Bob is kind. Bob is smart. Bob is young. Fiona is cold. Fiona is smart. Fiona is young. Gary is cold. Gary is kind. Gary is young. Harry is big. Harry is cold. Harry is quiet. Harry is white. If Gary is cold then Gary is smart. If Harry is smart then Harry is not cold. If someone is smart then they are quiet. If someone is white and kind then they are smart. If Bob is white and Bob is not kind then Bob is quiet. If Gary is kind and Gary is quiet then Gary is big. If someone is big then they are white. If Fiona is quiet and Fiona is not young then Fiona is not big.
Bob is big.
("Bob" "is" "big" "+")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If Gary is cold then Gary is smart.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "smart" "+"))
If Harry is smart then Harry is not cold.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "cold" "-"))
If someone is smart then they are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white and kind then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Bob is white and Bob is not kind then Bob is quiet.
((("Bob" "is" "white" "+") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "quiet" "+"))
If Gary is kind and Gary is quiet then Gary is big.
((("Gary" "is" "kind" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "big" "+"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If Fiona is quiet and Fiona is not young then Fiona is not big.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "young" "~")) -> ("Fiona" "is" "big" "-"))
Gary is kind.
True
1
proof
[(triple10)]
("Gary" "is" "kind" "+")
triple10
Bob is not young.
False
1
inv-proof
[(triple5)]
("Bob" "is" "young" "-")
triple5
Bob is quiet.
True
2
proof
[(((triple4) -> rule3) OR ((((((triple1) -> rule7) triple3) -> rule4)) -> rule3))]
("Bob" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((((triple1) -> (rule7 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Fiona is not quiet.
False
2
inv-proof
[(((triple7) -> rule3))]
("Fiona" "is" "quiet" "-")
((triple7) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple9) -> rule1)) -> rule3))]
("Gary" "is" "quiet" "+")
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule3))]
("Gary" "is" "quiet" "-")
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "smart" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "white" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is kind.[(triple3)] Bob is not cold.[(triple2)] Bob is smart.[(triple4 OR ((((triple1) -> rule7) triple3) -> rule4))] Bob is young.[(triple5)] Fiona is cold.[(triple6)] Fiona is smart.[(triple7)] Fiona is young.[(triple8)] Gary is cold.[(triple9)] Gary is kind.[(triple10)] Gary is young.[(triple11)] Harry is big.[(triple12)] Harry is cold.[(triple13)] Harry is quiet.[(triple14)] Harry is white.[(triple15 OR ((triple12) -> rule7))] @1: Bob is quiet.[(((triple4) -> rule3) OR ((((((triple1) -> rule7) triple3) -> rule4)) -> rule3))] Bob is white.[(((triple1) -> rule7))] Fiona is quiet.[(((triple7) -> rule3))] Gary is smart.[(((triple9) -> rule1))] @2: Gary is quiet.[(((((triple9) -> rule1)) -> rule3))] @3: Gary is big.[(((triple10 ((((triple9) -> rule1)) -> rule3)) -> rule6))] @4: Gary is white.[(((((triple10 ((((triple9) -> rule1)) -> rule3)) -> rule6)) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not cold.
("Bob" "is" "cold" "-")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((((triple1) -> (rule7 % int2)) triple3) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple5
Fiona is cold.
("Fiona" "is" "cold" "+")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
Fiona is young.
("Fiona" "is" "young" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is young.
("Gary" "is" "young" "+")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple12) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((((triple1) -> (rule7 % int3)) triple3) -> (rule4 % int2))) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple7) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple9) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((triple10 ((((triple9) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((triple10 ((((triple9) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4